Termination w.r.t. Q proof of TRS/Cimeintersect.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(app(l1, l2), l3) → APP(l2, l3)
MEM(x, cons(y, l)) → EQ(x, y)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → INTER(l1, l3)
INTER(l1, cons(x, l2)) → MEM(x, l1)
MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
INTER(l1, app(l2, l3)) → APP(inter(l1, l2), inter(l1, l3))
IFMEM(false, x, l) → MEM(x, l)
INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)
EQ(s(x), s(y)) → EQ(x, y)
INTER(l1, app(l2, l3)) → INTER(l1, l3)
INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) → INTER(l1, l2)
INTER(app(l1, l2), l3) → APP(inter(l1, l3), inter(l2, l3))
INTER(cons(x, l1), l2) → MEM(x, l2)
APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
IFINTER(false, x, l1, l2) → INTER(l1, l2)
APP(cons(x, l1), l2) → APP(l1, l2)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(l1, l2), l3) → APP(l2, l3)
MEM(x, cons(y, l)) → EQ(x, y)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → INTER(l1, l3)
INTER(l1, cons(x, l2)) → MEM(x, l1)
MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
INTER(l1, app(l2, l3)) → APP(inter(l1, l2), inter(l1, l3))
IFMEM(false, x, l) → MEM(x, l)
INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)
EQ(s(x), s(y)) → EQ(x, y)
INTER(l1, app(l2, l3)) → INTER(l1, l3)
INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) → INTER(l1, l2)
INTER(app(l1, l2), l3) → APP(inter(l1, l3), inter(l2, l3))
INTER(cons(x, l1), l2) → MEM(x, l2)
APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
IFINTER(false, x, l1, l2) → INTER(l1, l2)
APP(cons(x, l1), l2) → APP(l1, l2)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MEM(x, cons(y, l)) → EQ(x, y)
APP(app(l1, l2), l3) → APP(l2, l3)
INTER(app(l1, l2), l3) → INTER(l2, l3)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
INTER(app(l1, l2), l3) → INTER(l1, l3)
INTER(l1, cons(x, l2)) → MEM(x, l1)
INTER(l1, app(l2, l3)) → APP(inter(l1, l2), inter(l1, l3))
MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
IFMEM(false, x, l) → MEM(x, l)
INTER(l1, app(l2, l3)) → INTER(l1, l3)
EQ(s(x), s(y)) → EQ(x, y)
INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)
INTER(l1, app(l2, l3)) → INTER(l1, l2)
INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
INTER(app(l1, l2), l3) → APP(inter(l1, l3), inter(l2, l3))
INTER(cons(x, l1), l2) → MEM(x, l2)
APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
APP(cons(x, l1), l2) → APP(l1, l2)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 4 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(app(l1, l2), l3) → APP(l2, l3)
APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
APP(cons(x, l1), l2) → APP(l1, l2)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APP(app(l1, l2), l3) → APP(l2, l3)
APP(app(l1, l2), l3) → APP(l1, app(l2, l3))
APP(cons(x, l1), l2) → APP(l1, l2)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2) = APP(x1)
app(x1, x2) = app(x1, x2)
cons(x1, x2) = cons(x2)
nil = nil

Recursive Path Order [2].
Precedence:

app₂ > APP₁
cons₁ > APP₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

EQ(s(x), s(y)) → EQ(x, y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2) = EQ(x2)
s(x1) = s(x1)

Recursive Path Order [2].
Precedence:

s₁ > EQ₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
IFMEM(false, x, l) → MEM(x, l)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

MEM(x, cons(y, l)) → IFMEM(eq(x, y), x, l)
IFMEM(false, x, l) → MEM(x, l)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
MEM(x1, x2) = x2
cons(x1, x2) = cons(x2)
IFMEM(x1, x2, x3) = IFMEM(x3)
eq(x1, x2) = eq
false = false
s(x1) = s
0 = 0
true = true

Recursive Path Order [2].
Precedence:

cons₁ > IFMEM₁
cons₁ > eq

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)
INTER(l1, app(l2, l3)) → INTER(l1, l3)
INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) → INTER(l1, l2)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → INTER(l1, l3)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following rules:

if(true, x, y) → x
if(false, x, y) → y
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
app(app(l1, l2), l3) → app(l1, app(l2, l3))
mem(x, nil) → false
mem(x, cons(y, l)) → ifmem(eq(x, y), x, l)
ifmem(true, x, l) → true
ifmem(false, x, l) → mem(x, l)
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.